package il.ac.bgu.cs.heuristics.graph.pddl.auxiliary;

import il.ac.bgu.cs.heuristics.graph.pddl.parser.ExpressionParser;
import il.ac.bgu.cs.heuristics.graph.pddl.parser.types.AbstractParameter;
import il.ac.bgu.cs.heuristics.graph.pddl.parser.types.ITypedConstant;
import il.ac.bgu.cs.heuristics.graph.pddl.parser.types.LogicalOperator;
import il.ac.bgu.cs.heuristics.graph.pddl.parser.types.Predicate;
import il.ac.bgu.cs.heuristics.graph.types.ISubstitution;
import il.ac.bgu.cs.heuristics.utils.CollectionUtils;
import il.ac.bgu.cs.heuristics.utils.Validation;

import java.io.BufferedReader;
import java.io.IOException;
import java.io.InputStream;
import java.io.InputStreamReader;
import java.util.Collections;
import java.util.List;

/**
 * Resolves contradiction between substitution pairs
 * 
 * <p>
 * must be initialized with a standard contradictions input stream (txt file),
 * which contains contradictions rules.
 * 
 * <p>
 * Rules are comprised of predicates pairs which contradict. Each predicate can
 * have an operator, and must have only free parameters (prefixed with '?').<BR>
 * The order of parameters and logical operator is what's making the
 * contradiction logic
 * </p>
 * 
 * <p>
 * Predicate pairs must be delimited with a comma.<BR>
 * All types must be 'object' - meaning, does not support type contradictions
 * </p>
 * 
 * @see ISubstitution
 * @see Predicate
 * @see LogicalOperator
 * 
 * @author Ronen Pinko
 * 
 */
public class ContradictionResolver {
	private static final String			COMMENT_IDENTIFIER	= ";";

	/** the delimiter used to separate between two predicates in a rule */
	private final static String			RULE_DELIMITER		= ",";

	private final List<Contradiction>	contradictions		= CollectionUtils
																	.newArrayList();

	/**
	 * @param in
	 *            stream of the contradictions.txt input
	 * @throws IOException
	 *             if stream can't be read
	 * @throws IllegalArgumentException
	 *             if the contradictions format is malformed
	 */
	public ContradictionResolver(InputStream in) throws IOException,
			IllegalArgumentException {
		parse(Validation.ensureArgumentNeverNull(in));
	}

	public boolean resolve(ISubstitution sub1, ISubstitution sub2) {
		if (sub1.equals(sub2))
			return false;
		for (Contradiction contradiction : contradictions) {
			if (match(contradiction, sub1, sub2)) {
				return true;
			}
		}
		return false;
	}

	/**
	 * Returns {@code true} if the substitutions match the contradiction rule,
	 * meaning there is a contradiction
	 */
	private static boolean match(Contradiction contradiction,
			ISubstitution sub1, ISubstitution sub2) {
		if (canBeDismissed(contradiction, sub1, sub2)) {
			return false;
		}
		final List<Integer> occurIndices = CollectionUtils.newArrayList();
		final List<AbstractParameter> contradictionParams1 = contradiction.predicate1
				.getParameters();
		for (AbstractParameter param1 : contradictionParams1) {
			boolean foundParam = false;
			final List<AbstractParameter> contradictionParams2 = contradiction.predicate2
					.getParameters();
			for (AbstractParameter param2 : contradictionParams2) {
				if (param1.equals(param2)) {
					occurIndices.add(contradictionParams2.indexOf(param2));
					foundParam = true;
					break;
				}
			}
			if (!foundParam) {
				occurIndices.add(-1);
			}
		}

		int i = 0;
		for (ITypedConstant subConstant1 : sub1.getSubstitutedConstants()) {
			final Integer indexInOther = occurIndices.get(i++);
			if (indexInOther >= 0) {
				final ITypedConstant subConstant2 = sub2
						.getSubstitutedConstants().get(indexInOther);
				if (!subConstant1.equals(subConstant2)) {
					return false;
				}
			}
		}
		return true;
	}

	private static boolean canBeDismissed(Contradiction contradiction,
			ISubstitution sub1, ISubstitution sub2) {
		final Predicate subPredicate1 = sub1.getPredicate();
		final Predicate subPredicate2 = sub2.getPredicate();
		return !areSamePredicate(contradiction.predicate1, subPredicate1)
				|| !areSamePredicate(contradiction.predicate2, subPredicate2)
				|| operatorsContradict(contradiction.predicate1, subPredicate1)
				|| operatorsContradict(contradiction.predicate2, subPredicate2)
				|| Collections.disjoint(sub1.getSubstitutedConstants(), sub2
						.getSubstitutedConstants());
	}

	private static boolean areSamePredicate(Predicate p1, Predicate p2) {
		return p1.getName().equalsIgnoreCase(p2.getName());
	}

	private static boolean operatorsContradict(Predicate p1, Predicate p2) {
		return p1.getOperator().contradicts(p2.getOperator());
	}

	private void parse(InputStream in) throws IOException {
		final BufferedReader reader = new BufferedReader(new InputStreamReader(
				in));
		String line = reader.readLine();
		while (line != null) {
			parseLine(line.trim());
			line = reader.readLine();
		}
	}

	private void parseLine(String line) {
		if (line.isEmpty() || line.startsWith(COMMENT_IDENTIFIER)) {
			return;
		}
		final String[] rule = line.split(RULE_DELIMITER);
		if (rule.length != 2) {
			throw new IllegalArgumentException("malformed rule - " + line);
		}
		final Predicate predicate1 = ExpressionParser.parsePredicate(rule[0]);
		final Predicate predicate2 = ExpressionParser.parsePredicate(rule[1]);
		if (Collections.disjoint(predicate1.getParameters(), predicate2
				.getParameters())) {
			throw new IllegalArgumentException(
					"malformed rule (parameters must not be disjoint) - "
							+ line);
		}
		contradictions.add(new Contradiction(predicate1, predicate2));

	}

	private final static class Contradiction {
		private final Predicate	predicate1;
		private final Predicate	predicate2;

		Contradiction(Predicate predicate1, Predicate predicate2) {
			this.predicate1 = predicate1;
			this.predicate2 = predicate2;
		}
	}

}
